Inference at * 1 2 
Iof proof for Lemma absval ubound:

.....falsecase..... NILNIL

1. i : 
2. n : 
3. i < 0
  ((-i)  n)  (((-n)  i) & (i  n)) 

latex

 by (Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok SupInf:t) inil_term)
 b

latex

 .

Definitions	, t  T, P  Q, P  Q, P & Q, P  Q, x:A. B(x),
Lemmas	le wf